3.2 Permutation-argument
このあたりは線形代数の置換とかっぽい
回路のゲートは局所的に(現在の行または定義された相対行のセルに対してlocalに)動作するので、ゲートで使用するために任意のセルから現在の行に値をコピーする必要があったりする。この場合、コピー元とコピー先のセルが同じ値であることを強制する等値性制約(equality-constraint)が適用される。
この等式制約を実装するには、制約を表す並べ換え(permutation)を構成し、証明の中で並べ換えの引数を用いて制約を強制する
permutationは、集合をそれ自身に写す一対一写像である。順列は(サイクルの順序と各サイクルの回転まで)サイクルの合成に一意的に因数分解できる。
順列を書くときにサイクルの表記を使うことがある。(a b c)はaがbに、bがcに、cがaに対応するサイクルを表すとする(任意のサイズのサイクルへの一般化は明白である)。2つ以上のサイクルを隣り合わせに書くと、対応する並べ換えの合成を表す。例えば、(a b) (c d) は、aをbに、bをaに、cをdに、dをcに写す順列を表す。
Constructing the permutation
等式制約の集合に含まれる各変数の部分集合がサイクルを形成するような順列を構成したい。例えば、以下のような等式制約を定義した回路があるとする。
a≡b
a≡c
d≡e
この時、 equality-constraint set として{a,b,c} と {d,e}であり、permutation (a b c) (d e)を構築したい
Algorithm
我々は、不連続な集合であるサイクルの集合を追跡する必要がある。この問題に対する効率的なデータ構造が知られている。簡単のために、漸近的に最適ではないが、実装が容易なものを選択する。
現在の状態を以下のように表現する。
並べ換えそのものを表す配列マッピング
各サイクルの識別要素を追跡する補助配列Aux
各サイクルの大きさを記録する配列sizes
与えられたサイクルCの各要素xに対して、aux(x)は同じ要素c∈Cを指すという不変量がある。これにより、与えられた2つの要素xとyが同じサイクルにあるかどうか、aux(x)=aux(y)を確認することですぐに判断することができる。また、sizes(aux(x))はxを含むサイクルのサイズを与える(これはsizes(aux(x))に対してのみ保証され、sizes(x)に対しては保証されない)。
アルゴリズムは恒等順列の表現から始まる:すべてのxについて、mapping(x)=x, aux(x)=x, sizes(x)=1 とする。
等式制約を左≡右と追加する。
1. 左と右がすでに同じサイクルにあるかどうか、すなわち、aux(left)=aux(right)であるかどうかをチェックする。もしそうなら、何もすることはない。
2. そうでなければ、左と右は異なるサイクルに属している。sizes(aux(left))<sizes(aux(right)) ならば、左を大きいサイクル、右を小さいサイクルとする。
3. sizes(aux(left)):=sizes(aux(left))+sizes(aux(right)) を設定する。
4. 右の(小さい)サイクルのマッピングに従って、各要素 x に対して aux(x):=aux(left) をセットする。
5. mapping(left)とmapping(right)を交換することにより、小さいサイクルを大きいサイクルに分割する。
https://scrapbox.io/files/631843c7fed71500232a338d.png